\documentclass[handout]{beamer}

\usepackage{hyperref} 
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}

% AMSLaTeX packages
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amsfonts}

% we want to use images
\usepackage{graphicx}

\usepackage[]{listings}
\usepackage{beamerthemesplit}


% PDF settings
\hypersetup{%
	pdftitle={Verifying pattern matching with guards in Scala},%
	pdfauthor={Mirco Dotta, Philippe Suter},%
	pdfsubject={LARA},%
	pdfkeywords={LaTeX, Beamer, slides, pattern matching, Scala, guards, formal verification, disjointness, completeness}%
}

\title{Verifying pattern matching with guards in Scala}
\author{Mirco Dotta, Philippe Suter}
\date{\today\\ \tiny{version 1.1}}
\institute{
\inst{}EPFL --
SAV '07 }
% define some colors
\definecolor{ZurichBlue}{rgb}{.255,.41,.884} % RoyalBlue of svgnames
\definecolor{ZurichRed}{rgb}{0.8, 0, 0} % Red of svgnames
\definecolor{ZurichGreen}{rgb}{.196,.804,.196} % LimeGreen of svgnames
\definecolor{ZurichYellow}{rgb}{1,.648,0} % Orange of svgnames


\input{listingsScala}

\begin{document}
\lstset{language=scala, columns=fullflexible,showstringspaces=false,mathescape=true}

%\lstset{emph={cond,expr,value,pattern},emphstyle=\emph}   


% \begin{figure}[htbp]
%  	\begin{center}
%  	  \includegraphics[keepaspectratio=true,width=4cm]{img/scream.jpg}
%	\end{center}
%\end{figure}     

\frame{\titlepage}



%--------------------------------------------------%
%                  OUTLINE                               %
%--------------------------------------------------%
\begin{frame}[shrink=5]
\frametitle{Outline}
\tableofcontents
% You might wish to add the option [pausesections]
\end{frame}


%--------------------------------------------------%
%                  INTRODUCTION                  %
%--------------------------------------------------%

\section{Introduction}

% About SCALA
\subsection{Scala}
\begin{frame}[fragile]
\frametitle{Scala\footnote{\tiny{The Scala Experiment -- Can We Provide Better Language Support for Component Systems? \url{http://lamp.epfl.ch/~odersky/talks/google06.pdf}}}}
\begin{itemize}
	\item<1-> Scala is an object-oriented and functional language which is completely interoperable with Java.
	\item<2-> It removes some of the more arcane constructs of these environments and adds instead:
	\begin{enumerate}
		\item<2-> a uniform object model
		\item<2-> pattern matching and higher-order functions
		\item<2-> novel ways to abstract and compose programs
	\end{enumerate}
\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{Algebraic Data Types in Scala}

\begin{itemize}
	\item Consider the following ADT definition:
\end{itemize}

\begin{lstlisting}
type Tree  = Node of Tree * int * Tree
           | EmptyTree
\end{lstlisting}	

\pause

\begin{itemize}
	\item In Scala:
\end{itemize}

\pause

\begin{lstlisting}
abstract class Tree
\end{lstlisting}	


\begin{lstlisting}
case class Node (left: Tree, value: Int, right: Tree) extends Tree
\end{lstlisting}	


\begin{lstlisting}
case object EmptyTree extends Tree
\end{lstlisting}	


\end{frame}

% Pattern matching
\begin{frame}[fragile,label=search]
\frametitle{Pattern matching in Scala}

Consider the following search function on a sorted binary tree:

\pause



\begin{lstlisting}
def search(tree: Tree, value: Int): Boolean = tree match {	
    case EmptyTree $\Rightarrow$ false
    case Node(_,v,_) if(v == value) $\Rightarrow$ true
    case Node(l,v,_)  if(v < value) $\Rightarrow$ search(l,v) 
    case Node(_,v,r)  if(v > value) $\Rightarrow$ search(r,v)
    case _ $\Rightarrow$ throw new Exception("...")
}
\end{lstlisting}

%\hyperlink{status<6>}{\beamergotobutton{back}}

\end{frame}

\begin{frame}[fragile]
\frametitle{Pattern matching in Scala - cont'd}

You can:
\begin{itemize}
	\item<2-> match on objects
	\item<3-> {use recursive patterns
		\begin{lstlisting}
case Node(Node(_,5,_),_,_) $\Rightarrow$ output("5 on its left!")
		\end{lstlisting}
	}
	\item<4-> {use type restrictions
		\begin{lstlisting}
case Node(left: Node,_,_) $\Rightarrow$ output("node on its left!")
		\end{lstlisting}
	}
	\item<5-> use guards
	\item<6-> use wildcards
\end{itemize}


\end{frame}


% Properties we want to verify
\subsection{reasoning about pattern matching}
\begin{frame}[fragile]
\frametitle{Pattern matching}

In general, two interesting properties: 
 
 \begin{itemize}
 	\item<2-> completeness
	\item<2-> disjointness
 \end{itemize}
 
\uncover<3-> {(both $\Rightarrow$ partitioning)}
 
 \bigskip
 
\uncover<4->{Enforcement of these properties varies among languages.}

\end{frame}

% Scala Status
\subsection{status in Scala}
\begin{frame}[fragile,label=status]
\frametitle{Status in Scala}

In Scala:
\begin{itemize}
	\item<2-> completeness is not required
	\begin{itemize}
		\item<3-> \texttt{\textcolor{ZurichRed}{MatchException}} raised if no match is found
	\end{itemize}
	
	\item<4-> completeness can be checked to some extent
	\begin{itemize}
		\item<5-> only for \textbf{sealed} classes
		\item<6-> guards are taken into account very conservatively
		%\hyperlink{search<2>}{\beamergotobutton{example}}
	\end{itemize}
	
	\item<7-> disjointness is neither required nor checkable
	
	\item<8-> unreachable patterns are forbidden 
\end{itemize}

\end{frame}

% Motivation
\subsection{motivation}
\begin{frame}[fragile]
\frametitle{Scala status - cont'd}

Current situation:
\begin{itemize}
	\item<2-> little help from compiler 
		\begin{itemize}
			\item<2-> too conservative
		 	\item<2-> Scala users keep asking for improved completeness checks			
		\end{itemize}
	
	\item<3-> ensuring disjointness is left to the developers
	
\end{itemize}

\bigskip

\uncover<4->{There is room for improvements using formal verification techniques.}

\end{frame}


% Big picture
\subsection{project overview}
\begin{frame}[fragile]
\frametitle{Extending the Scala compiler}

\begin{enumerate}
\item Analysis is implemented as an additional phase in the compiler.

\item Pattern matching subtrees and the related hierarchy are retrieved from the compiler environment and AST.

\item This information is used to generate an intermediate representation.

\item From there, formulas are constructed and fed to formDecider.

\item Based on the results, warning/error messages are sent back to the compiler.
\end{enumerate}

\end{frame}

\begin{frame}
\frametitle{The big picture}
 \begin{figure}[htbp]
  	\begin{center}
  	  \includegraphics[keepaspectratio=true,heigth=5cm]{img/bigpicture.pdf}
	\end{center}
\end{figure}    

\end{frame}

%--------------------------------------------------%
%         TRANSFORM PATTERNS           %
%--------------------------------------------------%
\section{Turning patterns into formulas}

% Patterns to formula: problematics
\subsection{general idea}
\begin{frame}[fragile]
\frametitle{From patterns to formulas}
\begin{itemize}
	\item<1-> We want to create formulas -- in \emph{FOPL} -- to prove completeness and disjointness.
	\item<2-> The process takes two aspects: 
	\begin{itemize}	
		\item<3-> define a mapping from pattern expressions to formulas 
		\begin{itemize}
			\item<4-> how to represent types of classes and objects? 
			\item<4-> how to represent constructor parameters?
			\item<4-> how to deal with recursive constructs?
			\item<4-> how to include guards?
			\item<4-> how about primitive types? and strings?
		\end{itemize}
		
		\item<5-> define completeness and disjointness 
		\begin{itemize}
			\item<6-> what axioms do we need?
			\item<6-> how do formulas relate to each other? 
		\end{itemize}
	\end{itemize}
\end{itemize}

\end{frame}

% Patterns to formula: problematics
\subsection{formalization of concepts}
\begin{frame}[fragile]
\frametitle{Formalizing completeness and disjointness}

Consider a pattern-matching expression $E$:
\begin{lstlisting}
$t$ match {
    case $p_1$ $\Rightarrow$ $\ldots$
    $\ldots$
    case $p_i$ $\Rightarrow$ $\ldots$
}
\end{lstlisting}

\pause

Assume we have a predicate $\xi(t, p)$ such that $\forall i$, $\xi(t,p_i)$ is true iff the pattern $p_i$ matches the expression $t$.

\begin{itemize}
	\item<3-> $E$ is complete $\iff$ $\bigvee_i \xi(t,p_i)$
	\item<4-> $E$ is disjoint $\iff$ $\forall i,j$, $i \neq j \implies \neg(\xi(t,p_i) \wedge \xi(t,p_j))$
\end{itemize}
\end{frame}


\begin{frame}[fragile]
\frametitle{Formalizing patterns}

Types can naturally be represented as sets
\begin{itemize}\item t: Node $\longmapsto$ $t \in Node$\end{itemize}

\bigskip
\pause

Subtyping can be seen as set inclusion
\begin{itemize}\item \textbf{case class} Node(...) \textbf{extends} Tree $\longmapsto$ $Node \subseteq Tree$\end{itemize}

\bigskip
\pause

Properties of ADT are used to generate axioms
\begin{itemize}\item $\forall t \in Tree, t \in Node(...) \oplus t \in EmptyTree$\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{Formalizing patterns -- cont'd}

Objects are represented as singletons
\begin{itemize} \item \textbf{case object} Leaf $\longmapsto Leaf = \{leaf_0\}$ \end{itemize}

\bigskip
\pause

Types of constructor parameters are represented by functions
\begin{itemize} \item \textbf{case class} Node(left: Tree, right: Tree) $\longmapsto$ $\forall n \in Node~ (\Psi_{\text{\tiny{Node,left}}}(n) \in Tree \wedge \Psi_{\text{\tiny{Node,right}}} \in Tree)$\end{itemize}

\bigskip
\pause

The above transformations, along with the information about the selector's type, define \emph{axioms} about $E$.

\end{frame}

\subsection{axioms}
\begin{frame}[fragile]
\frametitle{Example -- Axioms}

\begin{lstlisting}
abstract class Tree
case class Node(left:Tree,right:Tree) extends Tree
case object Leaf extends Tree

t: Tree match { $\ldots$ }
\end{lstlisting}

\begin{align*}
t & \in Tree \\
  & \wedge Node \subseteq Tree \wedge Leaf \subseteq Tree \wedge Leaf = \{leaf_0\} \\
  & \wedge \forall t_0 \in Tree, t_0 \in Node(...) \oplus t_0 \in Leaf \\
  & \wedge  \forall n \in Node~ (\Psi_{\text{\tiny{Node,left}}}(n) \in Tree \wedge \Psi_{\text{\tiny{Node,right}}} \in Tree)
\end{align*}
\end{frame}

\begin{frame}[fragile]
\frametitle{Axioms -- cont'd}

Recall that the formulas $\xi(t,p_i)$ correspond to the patterns $p_i$.

\begin{itemize}
\item<2-> Each of these formulas is in the form $A(t) \implies \Pi(p_i)$, where $A(t)$ are the axioms previously mentioned, and $\Pi(p_i)$ a formula depending on $p_i$.

\item<3-> The formula for completeness $\bigvee_i \xi(t,p_i)$ hence becomes $\bigvee_i (A(t) \implies \Pi(p_i))$
\end{itemize}

\bigskip

\uncover<4->{Simplified, this becomes: $A(t) \implies \bigvee_i \Pi(p_i)$}

\end{frame}

\subsection{patterns}
\begin{frame}[fragile]
\frametitle{Translation of patterns}
The ``root'' type in the pattern is assigned to the selector
\begin{itemize} \item t \textbf{match} \{ \textbf{case} Node(\ldots) $\Rightarrow$ \ldots \} $\longmapsto t \in Node$ \end{itemize}

\bigskip
\pause

Aliases\footnote{\tiny{the practical implementation slightly differs when proving completeness}} are bound to fresh names
\begin{itemize} \item \textbf{case} Node(left: Node, \ldots) $\Rightarrow \ldots$ \\ $\qquad \longmapsto left_{\text{\tiny{fresh}}} =  \Psi_{\text{\tiny{Node,left}}}(t) \wedge left_{\text{\tiny{fresh}}} \in Node$ \end{itemize}

\bigskip
\pause

Wildcards generate no constraints
\begin{itemize} \item \textbf{case} \_ $\Rightarrow \ldots \longmapsto true$ \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Translation of patterns -- cont'd}

Guards are, to some extent, translated to formulas:
\begin{itemize}
	\item equality and arithmetic operators are kept ``as it''
	\item \texttt{equals} is always considered side-effect free 
	\item {dynamic type tests are converted to set membership
		\begin{itemize} \item \texttt{o.isInstanceOf[\emph{Type}]} $\longmapsto$  $o \in Type$\end{itemize}}
	\item other method calls are ignored
\end{itemize}

\pause
\bigskip

The result of the transformation is a predicate, whose parameters are the selector and the aliases defined in the pattern.

\bigskip

It is added as a conjunction to the main formula.
\end{frame}

\subsection{miscellaneous}
\begin{frame}[fragile]
\frametitle{Matching on lists}
Scala, as a language making an extensive use of lists, has a dedicated syntax for them:

\begin{lstlisting}
z match {
    case Nil $\Rightarrow \ldots$
    case x :: xs $\Rightarrow \ldots$
}
\end{lstlisting}

\ldots but this is essentially syntactic sugar for the following hierarchy:

\begin{lstlisting}
sealed abstract class List
case final class ::(List, List) extends List
case object Nil extends List
\end{lstlisting}
\end{frame}


%--------------------------------------------------%
%                     IMPLEMENTATION          %
%--------------------------------------------------%
\section{Implementation}

\subsection{current status}
\begin{frame}
\frametitle{Implementation status}
\begin{itemize}
	\item large supported subset of Scala pattern matching expressions
	\item generation of formulas for completeness and disjointness 
	\item integration with formDecider
	\item scalac integration under way \ldots
\end{itemize}
\end{frame}

\subsection{future work}
\begin{frame}[fragile]
\frametitle{Future work}

Some issues we want to address in the future:

\begin{itemize}
	\item \ldots complete scalac integration :)
	\item allow matching on string constants
	\item improve support for primitive types
	\item implement limited support for external variables and functions
	\item<2-> \ldots oh, well, you always find something to do
\end{itemize}

\end{frame}

\begin{frame}
Questions ?
\end{frame}

\begin{frame}[fragile]
\frametitle{One for the road\ldots}
\begin{lstlisting}
sealed abstract class Arith
case class Sum(l: Arith, r: Arith) extends Arith
case class Prod(n: Num, f: Arith) extends Arith
case class Num(n: Int) extends Arith

def eval(a: Arith): Int = (a: @verified) match {
    case Sum(l, r) => eval(l) + eval(r)
    case Prod(Num(n), f) if(n == 0) => 0
    case Prod(Num(n), f) if(n != 0) => n * eval(f)
    case Num(n) => n
}
\end{lstlisting} 
\end{frame}

\begin{frame}
\begin{align*}
a & \in Arith \wedge Sum \subseteq Arith \wedge Prod \subseteq Arith \wedge Num \subseteq Arith \\
  & \wedge \forall a_0 \in Arith, ((a_0 \in Sum \oplus a_0 \in Prod) \wedge (a_0 \in Sum \oplus a_0 \in Num) \\
  & \wedge (a_0 \in Prod \oplus a_0 \in Num)) \wedge \forall s_0 \in Sum, (\Psi_{\text{\tiny{Sum,l}}}(s_0) \in Arith \\
 & \wedge \Psi_{\text{\tiny{Sum,r}}}(s_0) \in Arith) \wedge \forall p_0 \in Prod, (\Psi_{\text{\tiny{Prod,n}}}(p_0) \in Num \\
  & \wedge \Psi_{\text{\tiny{Prod,f}}}(s_0) \in Arith) \wedge \forall n_0 \in Num, \Psi_{\text{\tiny{Num,n}}}(n_0) \in \mathbb{N} \\
\implies & \\
       &((l_{\text{\tiny{fresh}}} = \Psi_{\text{\tiny{Sum,l}}}(a) \wedge r_{\text{\tiny{fresh}}} = \Psi_{\text{\tiny{Sum,r}}}(a)) \implies a \in Sum)  \\
%
\vee &((f_{\text{\tiny{fresh}}} = \Psi_{\text{\tiny{Prod,f}}}(a) \wedge n_{\text{\tiny{fresh}}} = \Psi_{\text{\tiny{Num,n}}}(\Psi_{\text{\tiny{Prod,l}}}(a))) \implies a \in Prod \\
        & \wedge \Psi_{\text{\tiny{Prod,l}}}(a) \in Num \wedge n{\text{\tiny{fresh}}} = 0) \\
%
\vee &((f_{\text{\tiny{fresh'}}} = \Psi_{\text{\tiny{Prod,f}}}(a) \wedge n_{\text{\tiny{fresh'}}} = \Psi_{\text{\tiny{Num,n}}}(\Psi_{\text{\tiny{Prod,l}}}(a))) \implies a \in Prod \\
        & \wedge \Psi_{\text{\tiny{Prod,l}}}(a) \in Num \wedge n{\text{\tiny{fresh'}}} \neq 0) \\
%
\vee & (n_{\text{\tiny{fresh''}}} = \Psi_{\text{\tiny{Num,n}}}(a) \implies a \in Num)      
\end{align*}
\end{frame}

\end{document}
